|
In programming languages (especially functional programming languages) and type theory, an option type or maybe type is a polymorphic type that represents encapsulation of an optional value; e.g., it is used as the return type of functions which may or may not return a meaningful value when they are applied. It consists of either an empty constructor (called ''None'' or ''Nothing''), or a constructor encapsulating the original data type A (written ''Just'' A or ''Some'' A). Outside of functional programming, these are known as nullable types. * In the Haskell language, the option type (called ''Maybe'') is defined as . * In the Idris language, the option type is also defined as . * In the Agda language, the option type is called Maybe with variants nothing and just a.* In the Coq language, the option type is defined as . * In the OCaml language, the option type is defined as type 'a option = None | Some of 'a.* In the Scala language, the option type is defined as parameterized abstract class '.. Option() = if (x == null) None else Some(x)...* In the Standard ML language, the option type is defined as datatype 'a option = NONE | SOME of 'a.* In the Rust language, it is defined as enum Option.* In the Swift language, it is defined as enum Optional but is generally written as T? and is initialized with either a value or nil.* In the Julia language, the option type is called Nullable.* In the Java language since version 8, the option type is defined as parameterized final class Optional. * In the C++ language proposed extensions, the option type is defined as the template class template.In type theory, it may be written as: . In languages that have tagged unions, as in most functional programming languages, option types can be expressed as the tagged union of a unit type plus the encapsulated type. In the Curry-Howard correspondence, option types are related to the annihilation law for ∨: x∨1=1. An option type can also be seen as a collection containing either a single element or zero elements. == The option monad == The option type is a monad under the following functions: : : We may also describe the option monad in terms of functions ''return'', ''fmap'' and ''join'', where the latter two are given by: : : The option monad is an additive monad: it has ''Nothing'' as a zero constructor and the following function as a monadic sum: : In fact, the resulting structure is an idempotent monoid. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「option type」の詳細全文を読む スポンサード リンク
|